Inference at * 
Iof proof for Lemma before-adjacent:


  T:Type, L:(T List), x, y:T.
  no_repeats(T;L)
   adjacent(T;L;x;y)
   (z:T. z before y  L  (z before x  L  (z = x))) 

latex

 by ((InductionOnList) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 1. T : Type
C1: 2. T List
C1: 3. x : T
C1: 4. y : T
C1: 5. no_repeats(T;[])
C1: 6. adjacent(T;[];x;y)
C1: 7. z : T
C1: 8. z before y  []
C1:   z before x  []  (z = x)
C2: 

C2: 1. T : Type
C2: 2. T List
C2: 3. u : T
C2: 4. v : T List
C2: 5. x, y:T.
C2: 5. no_repeats(T;v)  adjacent(T;v;x;y)  (z:T. z before y  v  (z before x  v  (z = x)))
C2: 6. x : T
C2: 7. y : T
C2: 8. no_repeats(T;[u / v])
C2: 9. adjacent(T;[u / v];x;y)
C2: 10. z : T
C2: 11. z before y  [u / v]
C2:   z before x  [u / v]  (z = x)
C.

Definitions	[], P  Q, P  Q, left + right, x before y  l, adjacent(T;L;x;y), Type, no_repeats(T;l), [car / cdr], x:A. B(x), x:AB(x), s = t, A List, type List, t  T
Lemmas	l before wf, adjacent wf, no repeats wf